\documentclass[12pt]{report}
\usepackage[utf8x]{inputenc}

%Warning: tipa declares many non-standard macros used by utf8x to
%interpret utf8 characters but extra packages might have to be added
%(e.g. "textgreek" for Greek letters not already in tipa).
%Use coqdoc's option -p to add new packages.
\usepackage{tipa}

\usepackage[T1]{fontenc}
\usepackage{fullpage}
\usepackage{coqdoc}
\usepackage{amsmath,amssymb}
\begin{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% This file has been automatically generated with the command
%% coqdoc -utf8 -o informe/LenguajeTex/Lenguaje.tex --latex Lenguaje.v 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\coqlibrary{Lenguaje}{Library }{Lenguaje}

\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Require} \coqdockw{Import} \coqexternalref{}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Arith.EqNat}{\coqdoclibrary{Arith.EqNat}}.\coqdoceol
\coqdocnoindent
\coqdockw{Set Implicit Arguments}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Module} \coqdockw{Type} \coqdef{Lenguaje.ITipos}{ITipos}{\coqdocmodule{ITipos}}.\coqdoceol
\coqdocemptyline
\end{coqdoccode}
Tipos de datos \begin{coqdoccode}
\coqdocnoindent
\coqdockw{Parameter} \coqdef{Lenguaje.ITipos.Bool}{Bool}{\coqdocaxiom{Bool}}    : \coqdockw{Set}.\coqdoceol
\coqdocnoindent
\coqdockw{Parameter} \coqdef{Lenguaje.ITipos.Integer}{Integer}{\coqdocaxiom{Integer}} : \coqdockw{Set}.\coqdoceol
\coqdocnoindent
\coqdockw{Parameter} \coqdef{Lenguaje.ITipos.Byte}{Byte}{\coqdocaxiom{Byte}}    : \coqdockw{Set}.\coqdoceol
\coqdocnoindent
\coqdockw{Parameter} \coqdef{Lenguaje.ITipos.Matrix}{Matrix}{\coqdocaxiom{Matrix}}  : \coqdockw{Set} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqdockw{Set}.\coqdoceol
\coqdocemptyline
\end{coqdoccode}
Constantes \begin{coqdoccode}
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.TRUE}{TRUE}{\coqdocvariable{TRUE}}  : \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.FALSE}{FALSE}{\coqdocvariable{FALSE}} : \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.ONE}{ONE}{\coqdocvariable{ONE}} : \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.ZERO}{ZERO}{\coqdocvariable{ZERO}} : \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}}.\coqdoceol
\coqdocemptyline
\end{coqdoccode}
Operaciones sobre Bool \begin{coqdoccode}
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.bool not}{bool\_not}{\coqdocvariable{bool\_not}} : \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.bool and}{bool\_and}{\coqdocvariable{bool\_and}} : \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.bool or}{bool\_or}{\coqdocvariable{bool\_or}}  : \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}}.\coqdoceol
\coqdocemptyline
\end{coqdoccode}
Operaciones sobre Integer \begin{coqdoccode}
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.int plus}{int\_plus}{\coqdocvariable{int\_plus}}   : \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.int minus}{int\_minus}{\coqdocvariable{int\_minus}}  : \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.int mult}{int\_mult}{\coqdocvariable{int\_mult}}   : \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.int div}{int\_div}{\coqdocvariable{int\_div}}    : \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.int modulo}{int\_modulo}{\coqdocvariable{int\_modulo}} : \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.int eq}{int\_eq}{\coqdocvariable{int\_eq}}     : \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.int lt}{int\_lt}{\coqdocvariable{int\_lt}}     : \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.int le}{int\_le}{\coqdocvariable{int\_le}}     : \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.int gt}{int\_gt}{\coqdocvariable{int\_gt}}     : \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.int ge}{int\_ge}{\coqdocvariable{int\_ge}}     : \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}}.\coqdoceol
\coqdocemptyline
\end{coqdoccode}
Operaciones sobre Byte \begin{coqdoccode}
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.byte xor}{byte\_xor}{\coqdocvariable{byte\_xor}} : \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}}   \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.byte shl}{byte\_shl}{\coqdocvariable{byte\_shl}} : \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.byte shr}{byte\_shr}{\coqdocvariable{byte\_shr}} : \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.byte and}{byte\_and}{\coqdocvariable{byte\_and}} : \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}}   \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.byte gt}{byte\_gt}{\coqdocvariable{byte\_gt}}  : \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}}   \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.byte eq}{byte\_eq}{\coqdocvariable{byte\_eq}}  : \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}}   \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}}.\coqdoceol
\coqdocemptyline
\end{coqdoccode}
Operaciones sobre Matrix \begin{coqdoccode}
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.matrix get}{matrix\_get}{\coqdocvariable{matrix\_get}} : \coqdockw{\ensuremath{\forall}} \coqdocvar{A} \coqdocvar{m} \coqdocvar{n}, \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Matrix}{\coqdocaxiom{Matrix}} \coqdocvariable{A} \coqdocvariable{m} \coqdocvariable{n} \ensuremath{\rightarrow} \coqexternalref{option}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocinductive{option}} \coqdocvariable{A}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.matrix set}{matrix\_set}{\coqdocvariable{matrix\_set}} : \coqdockw{\ensuremath{\forall}} \coqdocvar{A} \coqdocvar{m} \coqdocvar{n}, \coqref{Lenguaje.ITipos.Matrix}{\coqdocaxiom{Matrix}} \coqdocvariable{A} \coqdocvariable{m} \coqdocvariable{n} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqdocvariable{A} \ensuremath{\rightarrow} \coqexternalref{option}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocinductive{option}} (\coqref{Lenguaje.ITipos.Matrix}{\coqdocaxiom{Matrix}} \coqdocvariable{A} \coqdocvariable{m} \coqdocvariable{n}).\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.matrix zero}{matrix\_zero}{\coqdocvariable{matrix\_zero}} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{A}:\coqdockw{Set})(\coqdocvar{a}:\coqdocvariable{A}) \coqdocvar{m} \coqdocvar{n}, \coqref{Lenguaje.ITipos.Matrix}{\coqdocaxiom{Matrix}} \coqdocvariable{A} \coqdocvariable{m} \coqdocvariable{n}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{End} \coqref{Lenguaje}{\coqdocmodule{ITipos}}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Module} \coqdef{Lenguaje.Lenguaje}{Lenguaje}{\coqdocmodule{Lenguaje}} (\coqdocvar{ITs}: \coqref{Lenguaje}{\coqdocmodule{ITipos}}).\coqdoceol
\coqdocnoindent
\coqdockw{Import} \coqdocvar{ITs}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Inductive} \coqdef{Lenguaje.Lenguaje.Id}{Id}{\coqdocinductive{Id}} : \coqdockw{Set} := \coqdef{Lenguaje.Lenguaje.id}{id}{\coqdocconstructor{id}} : \coqexternalref{nat}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} \ensuremath{\rightarrow} \coqref{Lenguaje.Id}{\coqdocinductive{Id}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Lenguaje.Lenguaje.equal id}{equal\_id}{\coqdocdefinition{equal\_id}}(\coqdocvar{i} \coqdocvar{i'}: \coqref{Lenguaje.Lenguaje.Id}{\coqdocinductive{Id}}) :=\coqdoceol
\coqdocindent{1.00em}
\coqdockw{match} \coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocnotation{(}}\coqdocvariable{i}\coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocnotation{,}} \coqdocvariable{i'}\coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocnotation{)}} \coqdockw{with}\coqdoceol
\coqdocindent{2.00em}
\coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocnotation{(}}\coqref{Lenguaje.Lenguaje.id}{\coqdocconstructor{id}} \coqdocvar{n}\coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocnotation{,}} \coqref{Lenguaje.Lenguaje.id}{\coqdocconstructor{id}} \coqdocvar{n'}\coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocnotation{)}} \ensuremath{\Rightarrow} \coqexternalref{beq nat}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Arith.EqNat}{\coqdocdefinition{beq\_nat}} \coqdocvar{n} \coqdocvar{n'}\coqdoceol
\coqdocindent{1.00em}
\coqdockw{end}\coqdoceol
\coqdocnoindent
.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Inductive} \coqdef{Lenguaje.Lenguaje.ArithExp}{ArithExp}{\coqdocinductive{ArithExp}} : \coqdockw{Set} := \coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.arith exp num}{arith\_exp\_num}{\coqdocconstructor{arith\_exp\_num}}   : \coqref{Lenguaje.ITs.Integer}{\coqdocaxiom{Integer}}  \ensuremath{\rightarrow} \coqref{Lenguaje.ArithExp}{\coqdocinductive{ArithExp}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.arith exp id}{arith\_exp\_id}{\coqdocconstructor{arith\_exp\_id}}    : \coqref{Lenguaje.Lenguaje.Id}{\coqdocinductive{Id}}       \ensuremath{\rightarrow} \coqref{Lenguaje.ArithExp}{\coqdocinductive{ArithExp}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.arith exp plus}{arith\_exp\_plus}{\coqdocconstructor{arith\_exp\_plus}}  : \coqref{Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.ArithExp}{\coqdocinductive{ArithExp}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.arith exp minus}{arith\_exp\_minus}{\coqdocconstructor{arith\_exp\_minus}} : \coqref{Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.ArithExp}{\coqdocinductive{ArithExp}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.arith exp mult}{arith\_exp\_mult}{\coqdocconstructor{arith\_exp\_mult}}  : \coqref{Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.ArithExp}{\coqdocinductive{ArithExp}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.arith exp div}{arith\_exp\_div}{\coqdocconstructor{arith\_exp\_div}}   : \coqref{Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.ArithExp}{\coqdocinductive{ArithExp}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.arith exp mod}{arith\_exp\_mod}{\coqdocconstructor{arith\_exp\_mod}}   : \coqref{Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.ArithExp}{\coqdocinductive{ArithExp}}\coqdoceol
\coqdocnoindent
.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Infix} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:x '+' x}{"}{"}+" := \coqref{Lenguaje.Lenguaje.arith exp plus}{\coqdocconstructor{arith\_exp\_plus}} : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocnoindent
\coqdockw{Infix} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:x '-' x}{"}{"}-" := \coqref{Lenguaje.Lenguaje.arith exp minus}{\coqdocconstructor{arith\_exp\_minus}} : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocnoindent
\coqdockw{Infix} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:x '*' x}{"}{"}\ensuremath{\times}" := \coqref{Lenguaje.Lenguaje.arith exp mult}{\coqdocconstructor{arith\_exp\_mult}} : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocnoindent
\coqdockw{Infix} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:x '/' x}{"}{"}/" := \coqref{Lenguaje.Lenguaje.arith exp div}{\coqdocconstructor{arith\_exp\_div}} : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocnoindent
\coqdockw{Infix} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:x 'x25' x}{"}{"}\%" := \coqref{Lenguaje.Lenguaje.arith exp mod}{\coqdocconstructor{arith\_exp\_mod}} (\coqdoctac{at} \coqdockw{level} 69) : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Coercion} \coqref{Lenguaje.Lenguaje.arith exp id}{\coqdocconstructor{arith\_exp\_id}} : \coqdocvar{Id} >-> \coqdocvar{ArithExp}.\coqdoceol
\coqdocnoindent
\coqdockw{Coercion} \coqref{Lenguaje.Lenguaje.arith exp num}{\coqdocconstructor{arith\_exp\_num}} : \coqdocvar{Integer} >-> \coqdocvar{ArithExp}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Inductive} \coqdef{Lenguaje.Lenguaje.MatrixExp}{MatrixExp}{\coqdocinductive{MatrixExp}}: \coqdockw{Type} :=\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.matrix exp init}{matrix\_exp\_init}{\coqdocconstructor{matrix\_exp\_init}} : \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.MatrixExp}{\coqdocinductive{MatrixExp}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.matrix exp lit}{matrix\_exp\_lit}{\coqdocconstructor{matrix\_exp\_lit}}  : \coqdockw{\ensuremath{\forall}} \coqdocvar{A} \coqdocvar{m} \coqdocvar{n}, \coqref{Lenguaje.ITs.Matrix}{\coqdocaxiom{Matrix}} \coqdocvariable{A} \coqdocvariable{m} \coqdocvariable{n} \ensuremath{\rightarrow} \coqref{Lenguaje.MatrixExp}{\coqdocinductive{MatrixExp}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.matrix exp id}{matrix\_exp\_id}{\coqdocconstructor{matrix\_exp\_id}}   : \coqref{Lenguaje.Lenguaje.Id}{\coqdocinductive{Id}} \ensuremath{\rightarrow} \coqref{Lenguaje.MatrixExp}{\coqdocinductive{MatrixExp}}\coqdoceol
\coqdocnoindent
.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Coercion} \coqref{Lenguaje.Lenguaje.matrix exp id}{\coqdocconstructor{matrix\_exp\_id}} : \coqdocvar{Id} >-> \coqdocvar{MatrixExp}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Inductive} \coqdef{Lenguaje.Lenguaje.ByteExp}{ByteExp}{\coqdocinductive{ByteExp}} : \coqdockw{Type} :=\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.byte exp num}{byte\_exp\_num}{\coqdocconstructor{byte\_exp\_num}}    : \coqref{Lenguaje.ITs.Byte}{\coqdocaxiom{Byte}}      \ensuremath{\rightarrow} \coqref{Lenguaje.ByteExp}{\coqdocinductive{ByteExp}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.byte exp id}{byte\_exp\_id}{\coqdocconstructor{byte\_exp\_id}}     : \coqref{Lenguaje.Lenguaje.Id}{\coqdocinductive{Id}}        \ensuremath{\rightarrow} \coqref{Lenguaje.ByteExp}{\coqdocinductive{ByteExp}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.byte exp xor}{byte\_exp\_xor}{\coqdocconstructor{byte\_exp\_xor}}    : \coqref{Lenguaje.ByteExp}{\coqdocinductive{ByteExp}}   \ensuremath{\rightarrow} \coqref{Lenguaje.ByteExp}{\coqdocinductive{ByteExp}}  \ensuremath{\rightarrow} \coqref{Lenguaje.ByteExp}{\coqdocinductive{ByteExp}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.byte exp andbb}{byte\_exp\_andbb}{\coqdocconstructor{byte\_exp\_andbb}}  : \coqref{Lenguaje.ByteExp}{\coqdocinductive{ByteExp}}   \ensuremath{\rightarrow} \coqref{Lenguaje.ByteExp}{\coqdocinductive{ByteExp}}  \ensuremath{\rightarrow} \coqref{Lenguaje.ByteExp}{\coqdocinductive{ByteExp}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.byte exp shiftl}{byte\_exp\_shiftl}{\coqdocconstructor{byte\_exp\_shiftl}} : \coqref{Lenguaje.ByteExp}{\coqdocinductive{ByteExp}}   \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.ByteExp}{\coqdocinductive{ByteExp}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.byte exp shiftr}{byte\_exp\_shiftr}{\coqdocconstructor{byte\_exp\_shiftr}} : \coqref{Lenguaje.ByteExp}{\coqdocinductive{ByteExp}}   \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.ByteExp}{\coqdocinductive{ByteExp}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.byte exp matrix}{byte\_exp\_matrix}{\coqdocconstructor{byte\_exp\_matrix}} : \coqref{Lenguaje.Lenguaje.MatrixExp}{\coqdocinductive{MatrixExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.ByteExp}{\coqdocinductive{ByteExp}}\coqdoceol
\coqdocnoindent
.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Infix} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:x 'xor' x}{"}{"}xor" := \coqref{Lenguaje.Lenguaje.byte exp xor}{\coqdocconstructor{byte\_exp\_xor}} (\coqdoctac{at} \coqdockw{level} 79) : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocnoindent
\coqdockw{Infix} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:x 'and' x}{"}{"}and" := \coqref{Lenguaje.Lenguaje.byte exp andbb}{\coqdocconstructor{byte\_exp\_andbb}} (\coqdoctac{at} \coqdockw{level} 79) : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocnoindent
\coqdockw{Infix} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:x 'shl' x}{"}{"}shl" := \coqref{Lenguaje.Lenguaje.byte exp shiftl}{\coqdocconstructor{byte\_exp\_shiftl}} (\coqdoctac{at} \coqdockw{level} 79) : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocnoindent
\coqdockw{Infix} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:x 'shr' x}{"}{"}shr" := \coqref{Lenguaje.Lenguaje.byte exp shiftr}{\coqdocconstructor{byte\_exp\_shiftr}} (\coqdoctac{at} \coqdockw{level} 79) : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocnoindent
\coqdockw{Notation} \coqdef{Lenguaje.Lenguaje.::x '[' x '][' x ']'}{"}{"}m [ i ][ j ]" := (\coqref{Lenguaje.Lenguaje.byte exp matrix}{\coqdocconstructor{byte\_exp\_matrix}} \coqdocvar{m} \coqdocvar{i} \coqdocvar{j}) (\coqdoctac{at} \coqdockw{level} 70).\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Coercion} \coqref{Lenguaje.Lenguaje.byte exp num}{\coqdocconstructor{byte\_exp\_num}} : \coqdocvar{Byte} >-> \coqdocvar{ByteExp}.\coqdoceol
\coqdocnoindent
\coqdockw{Coercion} \coqref{Lenguaje.Lenguaje.byte exp id}{\coqdocconstructor{byte\_exp\_id}} : \coqdocvar{Id} >-> \coqdocvar{ByteExp}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Inductive} \coqdef{Lenguaje.Lenguaje.BoolExp}{BoolExp}{\coqdocinductive{BoolExp}} : \coqdockw{Type} := \coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.bool exp lit}{bool\_exp\_lit}{\coqdocconstructor{bool\_exp\_lit}} : \coqref{Lenguaje.ITs.Bool}{\coqdocaxiom{Bool}}     \ensuremath{\rightarrow} \coqref{Lenguaje.BoolExp}{\coqdocinductive{BoolExp}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.bool exp id}{bool\_exp\_id}{\coqdocconstructor{bool\_exp\_id}}  : \coqref{Lenguaje.Lenguaje.Id}{\coqdocinductive{Id}}       \ensuremath{\rightarrow} \coqref{Lenguaje.BoolExp}{\coqdocinductive{BoolExp}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.bool exp eq}{bool\_exp\_eq}{\coqdocconstructor{bool\_exp\_eq}}  : \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.BoolExp}{\coqdocinductive{BoolExp}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.bool exp lt}{bool\_exp\_lt}{\coqdocconstructor{bool\_exp\_lt}}  : \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.BoolExp}{\coqdocinductive{BoolExp}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.bool exp le}{bool\_exp\_le}{\coqdocconstructor{bool\_exp\_le}}  : \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.BoolExp}{\coqdocinductive{BoolExp}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.bool exp gt}{bool\_exp\_gt}{\coqdocconstructor{bool\_exp\_gt}}  : \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.BoolExp}{\coqdocinductive{BoolExp}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.bool exp gtb}{bool\_exp\_gtb}{\coqdocconstructor{bool\_exp\_gtb}} : \coqref{Lenguaje.Lenguaje.ByteExp}{\coqdocinductive{ByteExp}}  \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ByteExp}{\coqdocinductive{ByteExp}}  \ensuremath{\rightarrow} \coqref{Lenguaje.BoolExp}{\coqdocinductive{BoolExp}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.bool exp eqb}{bool\_exp\_eqb}{\coqdocconstructor{bool\_exp\_eqb}} : \coqref{Lenguaje.Lenguaje.ByteExp}{\coqdocinductive{ByteExp}}  \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ByteExp}{\coqdocinductive{ByteExp}}  \ensuremath{\rightarrow} \coqref{Lenguaje.BoolExp}{\coqdocinductive{BoolExp}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.bool exp ge}{bool\_exp\_ge}{\coqdocconstructor{bool\_exp\_ge}}  : \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.BoolExp}{\coqdocinductive{BoolExp}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.bool exp not}{bool\_exp\_not}{\coqdocconstructor{bool\_exp\_not}} : \coqref{Lenguaje.BoolExp}{\coqdocinductive{BoolExp}}  \ensuremath{\rightarrow} \coqref{Lenguaje.BoolExp}{\coqdocinductive{BoolExp}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.bool exp and}{bool\_exp\_and}{\coqdocconstructor{bool\_exp\_and}} : \coqref{Lenguaje.BoolExp}{\coqdocinductive{BoolExp}}  \ensuremath{\rightarrow} \coqref{Lenguaje.BoolExp}{\coqdocinductive{BoolExp}}  \ensuremath{\rightarrow} \coqref{Lenguaje.BoolExp}{\coqdocinductive{BoolExp}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.bool exp or}{bool\_exp\_or}{\coqdocconstructor{bool\_exp\_or}}  : \coqref{Lenguaje.BoolExp}{\coqdocinductive{BoolExp}}  \ensuremath{\rightarrow} \coqref{Lenguaje.BoolExp}{\coqdocinductive{BoolExp}}  \ensuremath{\rightarrow} \coqref{Lenguaje.BoolExp}{\coqdocinductive{BoolExp}}\coqdoceol
\coqdocnoindent
.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Infix} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:x '==' x}{"}{"}==" := \coqref{Lenguaje.Lenguaje.bool exp eq}{\coqdocconstructor{bool\_exp\_eq}} (\coqdoctac{at} \coqdockw{level} 79): \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocnoindent
\coqdockw{Infix} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:x 'lt' x}{"}{"}lt" := \coqref{Lenguaje.Lenguaje.bool exp lt}{\coqdocconstructor{bool\_exp\_lt}} (\coqdoctac{at} \coqdockw{level} 78) : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocnoindent
\coqdockw{Infix} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:x 'le' x}{"}{"}le" := \coqref{Lenguaje.Lenguaje.bool exp le}{\coqdocconstructor{bool\_exp\_le}} (\coqdoctac{at} \coqdockw{level} 78) : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocnoindent
\coqdockw{Infix} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:x 'gt' x}{"}{"}gt" := \coqref{Lenguaje.Lenguaje.bool exp gt}{\coqdocconstructor{bool\_exp\_gt}} (\coqdoctac{at} \coqdockw{level} 78) : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocnoindent
\coqdockw{Infix} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:x 'ge' x}{"}{"}ge" := \coqref{Lenguaje.Lenguaje.bool exp ge}{\coqdocconstructor{bool\_exp\_ge}} (\coqdoctac{at} \coqdockw{level} 78) : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocnoindent
\coqdockw{Notation} \coqdef{Lenguaje.Lenguaje.::'!'}{"}{"}!" := \coqref{Lenguaje.Lenguaje.bool exp not}{\coqdocconstructor{bool\_exp\_not}}.\coqdoceol
\coqdocnoindent
\coqdockw{Infix} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:x 'x26x26' x}{"}{"}\&\&" := \coqref{Lenguaje.Lenguaje.bool exp and}{\coqdocconstructor{bool\_exp\_and}} : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocnoindent
\coqdockw{Infix} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:x '||' x}{"}{"}||" := \coqref{Lenguaje.Lenguaje.bool exp or}{\coqdocconstructor{bool\_exp\_or}} : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Coercion} \coqref{Lenguaje.Lenguaje.bool exp id}{\coqdocconstructor{bool\_exp\_id}} : \coqdocvar{Id} >-> \coqdocvar{BoolExp}.\coqdoceol
\coqdocnoindent
\coqdockw{Coercion} \coqref{Lenguaje.Lenguaje.bool exp lit}{\coqdocconstructor{bool\_exp\_lit}} : \coqdocvar{Bool} >-> \coqdocvar{BoolExp}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Inductive} \coqdef{Lenguaje.Lenguaje.Val}{Val}{\coqdocinductive{Val}} : \coqdockw{Type} :=\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.bool val}{bool\_val}{\coqdocconstructor{bool\_val}}        : \coqref{Lenguaje.ITs.Bool}{\coqdocaxiom{Bool}}    \ensuremath{\rightarrow} \coqref{Lenguaje.Val}{\coqdocinductive{Val}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.int val}{int\_val}{\coqdocconstructor{int\_val}}         : \coqref{Lenguaje.ITs.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.Val}{\coqdocinductive{Val}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.byte val}{byte\_val}{\coqdocconstructor{byte\_val}}        : \coqref{Lenguaje.ITs.Byte}{\coqdocaxiom{Byte}}    \ensuremath{\rightarrow} \coqref{Lenguaje.Val}{\coqdocinductive{Val}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.byte matrix val}{byte\_matrix\_val}{\coqdocconstructor{byte\_matrix\_val}} : \coqdockw{\ensuremath{\forall}} \coqdocvar{m} \coqdocvar{n}, \coqref{Lenguaje.ITs.Matrix}{\coqdocaxiom{Matrix}} \coqref{Lenguaje.ITs.Byte}{\coqdocaxiom{Byte}} \coqdocvariable{m} \coqdocvariable{n} \ensuremath{\rightarrow} \coqref{Lenguaje.Val}{\coqdocinductive{Val}}\coqdoceol
\coqdocnoindent
.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Definition} \coqdef{Lenguaje.Lenguaje.State}{State}{\coqdocdefinition{State}} := \coqref{Lenguaje.Lenguaje.Id}{\coqdocinductive{Id}} \ensuremath{\rightarrow} \coqexternalref{option}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocinductive{option}} \coqref{Lenguaje.Lenguaje.Val}{\coqdocinductive{Val}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Lenguaje.Lenguaje.empty state}{empty\_state}{\coqdocdefinition{empty\_state}} : \coqref{Lenguaje.Lenguaje.State}{\coqdocdefinition{State}} := \coqdockw{fun} \coqdocvar{\_} \ensuremath{\Rightarrow} \coqexternalref{None}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{None}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Lenguaje.Lenguaje.Update}{Update}{\coqdocdefinition{Update}}(\coqdocvar{st}: \coqref{Lenguaje.Lenguaje.State}{\coqdocdefinition{State}})(\coqdocvar{id}: \coqref{Lenguaje.Lenguaje.Id}{\coqdocinductive{Id}})(\coqdocvar{val}: \coqref{Lenguaje.Lenguaje.Val}{\coqdocinductive{Val}}) : \coqref{Lenguaje.Lenguaje.State}{\coqdocdefinition{State}} :=\coqdoceol
\coqdocindent{1.00em}
\coqdockw{fun} (\coqdocvar{id'}: \coqref{Lenguaje.Lenguaje.Id}{\coqdocinductive{Id}}) \ensuremath{\Rightarrow} \coqdockw{if} (\coqref{Lenguaje.Lenguaje.equal id}{\coqdocdefinition{equal\_id}} \coqdocvariable{id} \coqdocvariable{id'}) \coqdockw{then} \coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} \coqdocvariable{val} \coqdockw{else} \coqdocvariable{st} \coqdocvariable{id'}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Inductive} \coqdef{Lenguaje.Lenguaje.ArithEval}{ArithEval}{\coqdocinductive{ArithEval}} (\coqdocvar{s}: \coqref{Lenguaje.Lenguaje.State}{\coqdocdefinition{State}}) : \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITs.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqdockw{Prop} :=\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.arith eval num}{arith\_eval\_num}{\coqdocconstructor{arith\_eval\_num}}   : \coqdockw{\ensuremath{\forall}} (\coqdocvar{n}:\coqref{Lenguaje.ITs.Integer}{\coqdocaxiom{Integer}}),\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.arith exp num}{\coqdocconstructor{arith\_exp\_num}} \coqdocvariable{n}) \coqdocvariable{n}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.arith eval id}{arith\_eval\_id}{\coqdocconstructor{arith\_eval\_id}}    : \coqdockw{\ensuremath{\forall}} (\coqdocvar{i}:\coqref{Lenguaje.Lenguaje.Id}{\coqdocinductive{Id}})(\coqdocvar{z}:\coqref{Lenguaje.ITs.Integer}{\coqdocaxiom{Integer}}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{s} \coqdocvariable{i} \coqexternalref{:type scope:x '=' x}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Logic}{\coqdocnotation{=}} \coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} (\coqref{Lenguaje.Lenguaje.int val}{\coqdocconstructor{int\_val}} \coqdocvariable{z}) \ensuremath{\rightarrow} \coqref{Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.arith exp id}{\coqdocconstructor{arith\_exp\_id}} \coqdocvariable{i})  \coqdocvariable{z}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.arith eval plus}{arith\_eval\_plus}{\coqdocconstructor{arith\_eval\_plus}}  : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}}) (\coqdocvar{n1} \coqdocvar{n2} : \coqref{Lenguaje.ITs.Integer}{\coqdocaxiom{Integer}}), \coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{e1} \coqdocvariable{n1} \ensuremath{\rightarrow} \coqref{Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{e2} \coqdocvariable{n2} \ensuremath{\rightarrow} \coqref{Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.arith exp plus}{\coqdocconstructor{arith\_exp\_plus}} \coqdocvariable{e1} \coqdocvariable{e2}) (\coqref{Lenguaje.ITs.int plus}{\coqdocaxiom{int\_plus}} \coqdocvariable{n1} \coqdocvariable{n2}) \coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.arith eval minus}{arith\_eval\_minus}{\coqdocconstructor{arith\_eval\_minus}} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}}) (\coqdocvar{n1} \coqdocvar{n2} : \coqref{Lenguaje.ITs.Integer}{\coqdocaxiom{Integer}}), \coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{e1} \coqdocvariable{n1} \ensuremath{\rightarrow} \coqref{Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{e2} \coqdocvariable{n2} \ensuremath{\rightarrow} \coqref{Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.arith exp minus}{\coqdocconstructor{arith\_exp\_minus}} \coqdocvariable{e1} \coqdocvariable{e2}) (\coqref{Lenguaje.ITs.int minus}{\coqdocaxiom{int\_minus}} \coqdocvariable{n1} \coqdocvariable{n2}) \coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.arith eval mult}{arith\_eval\_mult}{\coqdocconstructor{arith\_eval\_mult}}  : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}}) (\coqdocvar{n1} \coqdocvar{n2} : \coqref{Lenguaje.ITs.Integer}{\coqdocaxiom{Integer}}), \coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{e1} \coqdocvariable{n1} \ensuremath{\rightarrow} \coqref{Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{e2} \coqdocvariable{n2} \ensuremath{\rightarrow} \coqref{Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.arith exp mult}{\coqdocconstructor{arith\_exp\_mult}} \coqdocvariable{e1} \coqdocvariable{e2}) (\coqref{Lenguaje.ITs.int mult}{\coqdocaxiom{int\_mult}} \coqdocvariable{n1} \coqdocvariable{n2})\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.arith eval div}{arith\_eval\_div}{\coqdocconstructor{arith\_eval\_div}}   : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}}) (\coqdocvar{n1} \coqdocvar{n2} : \coqref{Lenguaje.ITs.Integer}{\coqdocaxiom{Integer}}),\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{e1} \coqdocvariable{n1} \ensuremath{\rightarrow} \coqref{Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{e2} \coqdocvariable{n2} \ensuremath{\rightarrow} \coqref{Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.arith exp div}{\coqdocconstructor{arith\_exp\_div}} \coqdocvariable{e1} \coqdocvariable{e2}) (\coqref{Lenguaje.ITs.int div}{\coqdocaxiom{int\_div}} \coqdocvariable{n1} \coqdocvariable{n2})\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.arith eval mod}{arith\_eval\_mod}{\coqdocconstructor{arith\_eval\_mod}}   : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}}) (\coqdocvar{n1} \coqdocvar{n2} : \coqref{Lenguaje.ITs.Integer}{\coqdocaxiom{Integer}}),\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{e1} \coqdocvariable{n1} \ensuremath{\rightarrow} \coqref{Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{e2} \coqdocvariable{n2} \ensuremath{\rightarrow} \coqref{Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.arith exp mod}{\coqdocconstructor{arith\_exp\_mod}} \coqdocvariable{e1} \coqdocvariable{e2}) (\coqref{Lenguaje.ITs.int modulo}{\coqdocaxiom{int\_modulo}} \coqdocvariable{n1} \coqdocvariable{n2})\coqdoceol
\coqdocnoindent
.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Inductive} \coqdef{Lenguaje.Lenguaje.MatrixEval}{MatrixEval}{\coqdocinductive{MatrixEval}} (\coqdocvar{s}: \coqref{Lenguaje.Lenguaje.State}{\coqdocdefinition{State}})(\coqdocvar{m} \coqdocvar{n}: \coqref{Lenguaje.ITs.Integer}{\coqdocaxiom{Integer}}) : \coqref{Lenguaje.Lenguaje.MatrixExp}{\coqdocinductive{MatrixExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITs.Matrix}{\coqdocaxiom{Matrix}} \coqref{Lenguaje.ITs.Byte}{\coqdocaxiom{Byte}} \coqdocvar{m} \coqdocvar{n} \ensuremath{\rightarrow} \coqdockw{Prop} :=\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.matrix eval lit}{matrix\_eval\_lit}{\coqdocconstructor{matrix\_eval\_lit}} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{mx}:\coqref{Lenguaje.ITs.Matrix}{\coqdocaxiom{Matrix}} \coqref{Lenguaje.ITs.Byte}{\coqdocaxiom{Byte}} \coqdocvar{m} \coqdocvar{n}),\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.MatrixEval}{\coqdocinductive{MatrixEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.matrix exp lit}{\coqdocconstructor{matrix\_exp\_lit}} \coqdocvariable{mx}) \coqdocvariable{mx}\coqdoceol
\coqdocindent{1.00em}
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.matrix eval id}{matrix\_eval\_id}{\coqdocconstructor{matrix\_eval\_id}} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{i}:\coqref{Lenguaje.Lenguaje.Id}{\coqdocinductive{Id}})(\coqdocvar{mx}:\coqref{Lenguaje.ITs.Matrix}{\coqdocaxiom{Matrix}} \coqref{Lenguaje.ITs.Byte}{\coqdocaxiom{Byte}} \coqdocvar{m} \coqdocvar{n}),\coqdoceol
\coqdocindent{2.00em}
\coqdocvar{s} \coqdocvariable{i} \coqexternalref{:type scope:x '=' x}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Logic}{\coqdocnotation{=}} \coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} (\coqref{Lenguaje.Lenguaje.byte matrix val}{\coqdocconstructor{byte\_matrix\_val}} \coqdocvariable{mx}) \ensuremath{\rightarrow} \coqref{Lenguaje.MatrixEval}{\coqdocinductive{MatrixEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.matrix exp id}{\coqdocconstructor{matrix\_exp\_id}} \coqdocvariable{i}) \coqdocvariable{mx}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.matrix eval init}{matrix\_eval\_init}{\coqdocconstructor{matrix\_eval\_init}} : \coqdockw{\ensuremath{\forall}} \coqdocvar{aexp1} \coqdocvar{aexp2} \coqdocvar{a},\coqdoceol
\coqdocindent{12.00em}
\coqref{Lenguaje.Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{aexp1} \coqdocvar{m} \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{aexp2} \coqdocvar{n} \ensuremath{\rightarrow}\coqdoceol
\coqdocindent{12.00em}
\coqref{Lenguaje.MatrixEval}{\coqdocinductive{MatrixEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.matrix exp init}{\coqdocconstructor{matrix\_exp\_init}} \coqdocvariable{aexp1} \coqdocvariable{aexp2}) (\coqref{Lenguaje.ITs.matrix zero}{\coqdocaxiom{matrix\_zero}} \coqdocvariable{a} \coqdocvar{m} \coqdocvar{n})\coqdoceol
\coqdocnoindent
.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Inductive} \coqdef{Lenguaje.Lenguaje.ByteEval}{ByteEval}{\coqdocinductive{ByteEval}} (\coqdocvar{s}: \coqref{Lenguaje.Lenguaje.State}{\coqdocdefinition{State}}) : \coqref{Lenguaje.Lenguaje.ByteExp}{\coqdocinductive{ByteExp}} \ensuremath{\rightarrow} \coqexternalref{option}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocinductive{option}} \coqref{Lenguaje.ITs.Byte}{\coqdocaxiom{Byte}} \ensuremath{\rightarrow} \coqdockw{Prop} :=\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.byte eval lit}{byte\_eval\_lit}{\coqdocconstructor{byte\_eval\_lit}} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{b}:\coqref{Lenguaje.ITs.Byte}{\coqdocaxiom{Byte}}),\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.ByteEval}{\coqdocinductive{ByteEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.byte exp num}{\coqdocconstructor{byte\_exp\_num}} \coqdocvariable{b}) (\coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} \coqdocvariable{b})\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.byte eval id}{byte\_eval\_id}{\coqdocconstructor{byte\_eval\_id}} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{i}:\coqref{Lenguaje.Lenguaje.Id}{\coqdocinductive{Id}})(\coqdocvar{b}:\coqref{Lenguaje.ITs.Byte}{\coqdocaxiom{Byte}}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{s} \coqdocvariable{i} \coqexternalref{:type scope:x '=' x}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Logic}{\coqdocnotation{=}} \coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} (\coqref{Lenguaje.Lenguaje.byte val}{\coqdocconstructor{byte\_val}} \coqdocvariable{b}) \ensuremath{\rightarrow} \coqref{Lenguaje.ByteEval}{\coqdocinductive{ByteEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.byte exp id}{\coqdocconstructor{byte\_exp\_id}} \coqdocvariable{i}) (\coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} \coqdocvariable{b})\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.byte eval xor}{byte\_eval\_xor}{\coqdocconstructor{byte\_eval\_xor}} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqref{Lenguaje.Lenguaje.ByteExp}{\coqdocinductive{ByteExp}})(\coqdocvar{b1} \coqdocvar{b2}: \coqref{Lenguaje.ITs.Byte}{\coqdocaxiom{Byte}}),\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.ByteEval}{\coqdocinductive{ByteEval}} \coqdocvar{s} \coqdocvariable{e1} (\coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} \coqdocvariable{b1}) \ensuremath{\rightarrow} \coqref{Lenguaje.ByteEval}{\coqdocinductive{ByteEval}} \coqdocvar{s} \coqdocvariable{e2} (\coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} \coqdocvariable{b2}) \ensuremath{\rightarrow} \coqref{Lenguaje.ByteEval}{\coqdocinductive{ByteEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.byte exp xor}{\coqdocconstructor{byte\_exp\_xor}} \coqdocvariable{e1} \coqdocvariable{e2}) (\coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} (\coqref{Lenguaje.ITs.byte xor}{\coqdocaxiom{byte\_xor}} \coqdocvariable{b1} \coqdocvariable{b2}))\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.50em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.byte eval andbb}{byte\_eval\_andbb}{\coqdocconstructor{byte\_eval\_andbb}} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqref{Lenguaje.Lenguaje.ByteExp}{\coqdocinductive{ByteExp}})(\coqdocvar{b1} \coqdocvar{b2}: \coqref{Lenguaje.ITs.Byte}{\coqdocaxiom{Byte}}),\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.ByteEval}{\coqdocinductive{ByteEval}} \coqdocvar{s} \coqdocvariable{e1} (\coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} \coqdocvariable{b1}) \ensuremath{\rightarrow} \coqref{Lenguaje.ByteEval}{\coqdocinductive{ByteEval}} \coqdocvar{s} \coqdocvariable{e2} (\coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} \coqdocvariable{b2}) \ensuremath{\rightarrow} \coqref{Lenguaje.ByteEval}{\coqdocinductive{ByteEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.byte exp andbb}{\coqdocconstructor{byte\_exp\_andbb}} \coqdocvariable{e1} \coqdocvariable{e2}) (\coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} (\coqref{Lenguaje.ITs.byte and}{\coqdocaxiom{byte\_and}} \coqdocvariable{b1} \coqdocvariable{b2}))\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.byte eval shiftl}{byte\_eval\_shiftl}{\coqdocconstructor{byte\_eval\_shiftl}} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e}: \coqref{Lenguaje.Lenguaje.ByteExp}{\coqdocinductive{ByteExp}})(\coqdocvar{x}: \coqref{Lenguaje.ITs.Integer}{\coqdocaxiom{Integer}})(\coqdocvar{n}: \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}})(\coqdocvar{b}: \coqref{Lenguaje.ITs.Byte}{\coqdocaxiom{Byte}}),\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.ByteEval}{\coqdocinductive{ByteEval}} \coqdocvar{s} \coqdocvariable{e} (\coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} \coqdocvariable{b}) \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{n} \coqdocvariable{x} \ensuremath{\rightarrow} \coqref{Lenguaje.ByteEval}{\coqdocinductive{ByteEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.byte exp shiftl}{\coqdocconstructor{byte\_exp\_shiftl}} \coqdocvariable{e} \coqdocvariable{n}) (\coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} (\coqref{Lenguaje.ITs.byte shl}{\coqdocaxiom{byte\_shl}} \coqdocvariable{b} \coqdocvariable{x}))\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.byte eval shiftr}{byte\_eval\_shiftr}{\coqdocconstructor{byte\_eval\_shiftr}} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e}: \coqref{Lenguaje.Lenguaje.ByteExp}{\coqdocinductive{ByteExp}})(\coqdocvar{x}: \coqref{Lenguaje.ITs.Integer}{\coqdocaxiom{Integer}})(\coqdocvar{n}: \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}})(\coqdocvar{b}: \coqref{Lenguaje.ITs.Byte}{\coqdocaxiom{Byte}}),\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.ByteEval}{\coqdocinductive{ByteEval}} \coqdocvar{s} \coqdocvariable{e} (\coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} \coqdocvariable{b}) \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{n} \coqdocvariable{x} \ensuremath{\rightarrow} \coqref{Lenguaje.ByteEval}{\coqdocinductive{ByteEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.byte exp shiftr}{\coqdocconstructor{byte\_exp\_shiftr}} \coqdocvariable{e} \coqdocvariable{n}) (\coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} (\coqref{Lenguaje.ITs.byte shr}{\coqdocaxiom{byte\_shr}} \coqdocvariable{b} \coqdocvariable{x}))\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.byte eval matrix}{byte\_eval\_matrix}{\coqdocconstructor{byte\_eval\_matrix}} : \coqdockw{\ensuremath{\forall}} \coqdocvar{aexp1} \coqdocvar{aexp2} (\coqdocvar{m} \coqdocvar{n} \coqdocvar{i} \coqdocvar{j}: \coqref{Lenguaje.ITs.Integer}{\coqdocaxiom{Integer}})(\coqdocvar{mexp}: \coqref{Lenguaje.Lenguaje.MatrixExp}{\coqdocinductive{MatrixExp}}) (\coqdocvar{matr}: \coqref{Lenguaje.ITs.Matrix}{\coqdocaxiom{Matrix}} \coqref{Lenguaje.ITs.Byte}{\coqdocaxiom{Byte}} \coqdocvariable{m} \coqdocvariable{n}),\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.Lenguaje.MatrixEval}{\coqdocinductive{MatrixEval}} \coqdocvar{s} \coqdocvariable{mexp} \coqdocvariable{matr} \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{aexp1} \coqdocvariable{i} \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{aexp2} \coqdocvariable{j} \ensuremath{\rightarrow} \coqref{Lenguaje.ByteEval}{\coqdocinductive{ByteEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.byte exp matrix}{\coqdocconstructor{byte\_exp\_matrix}} \coqdocvariable{mexp} \coqdocvariable{aexp1} \coqdocvariable{aexp2}) (\coqref{Lenguaje.ITs.matrix get}{\coqdocaxiom{matrix\_get}} \coqdocvariable{i} \coqdocvariable{j} \coqdocvariable{matr})\coqdoceol
\coqdocnoindent
.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Inductive} \coqdef{Lenguaje.Lenguaje.BoolEval}{BoolEval}{\coqdocinductive{BoolEval}} (\coqdocvar{s}: \coqref{Lenguaje.Lenguaje.State}{\coqdocdefinition{State}}) : \coqref{Lenguaje.Lenguaje.BoolExp}{\coqdocinductive{BoolExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITs.Bool}{\coqdocaxiom{Bool}} \ensuremath{\rightarrow} \coqdockw{Prop} :=\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.bool eval lit}{bool\_eval\_lit}{\coqdocconstructor{bool\_eval\_lit}} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{b}:\coqref{Lenguaje.ITs.Bool}{\coqdocaxiom{ITs.Bool}}),\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.BoolEval}{\coqdocinductive{BoolEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.bool exp lit}{\coqdocconstructor{bool\_exp\_lit}} \coqdocvariable{b}) \coqdocvariable{b}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.bool eval id}{bool\_eval\_id}{\coqdocconstructor{bool\_eval\_id}}  : \coqdockw{\ensuremath{\forall}} (\coqdocvar{i}:\coqref{Lenguaje.Lenguaje.Id}{\coqdocinductive{Id}})(\coqdocvar{b}:\coqref{Lenguaje.ITs.Bool}{\coqdocaxiom{Bool}}),\coqdoceol
\coqdocindent{3.50em}
\coqdocvar{s} \coqdocvariable{i} \coqexternalref{:type scope:x '=' x}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Logic}{\coqdocnotation{=}} \coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} (\coqref{Lenguaje.Lenguaje.bool val}{\coqdocconstructor{bool\_val}} \coqdocvariable{b}) \ensuremath{\rightarrow}  \coqref{Lenguaje.BoolEval}{\coqdocinductive{BoolEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.bool exp id}{\coqdocconstructor{bool\_exp\_id}} \coqdocvariable{i}) \coqdocvariable{b}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.bool eval eq}{bool\_eval\_eq}{\coqdocconstructor{bool\_eval\_eq}}  : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}})(\coqdocvar{n1} \coqdocvar{n2}: \coqref{Lenguaje.ITs.Integer}{\coqdocaxiom{Integer}}),\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{e1} \coqdocvariable{n1} \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{e2} \coqdocvariable{n2} \ensuremath{\rightarrow} \coqref{Lenguaje.BoolEval}{\coqdocinductive{BoolEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.bool exp eq}{\coqdocconstructor{bool\_exp\_eq}} \coqdocvariable{e1} \coqdocvariable{e2}) (\coqref{Lenguaje.ITs.int eq}{\coqdocaxiom{int\_eq}} \coqdocvariable{n1} \coqdocvariable{n2})\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.bool eval lt}{bool\_eval\_lt}{\coqdocconstructor{bool\_eval\_lt}}  : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}})(\coqdocvar{n1} \coqdocvar{n2}: \coqref{Lenguaje.ITs.Integer}{\coqdocaxiom{Integer}}),\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{e1} \coqdocvariable{n1} \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{e2} \coqdocvariable{n2} \ensuremath{\rightarrow} \coqref{Lenguaje.BoolEval}{\coqdocinductive{BoolEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.bool exp lt}{\coqdocconstructor{bool\_exp\_lt}} \coqdocvariable{e1} \coqdocvariable{e2}) (\coqref{Lenguaje.ITs.int lt}{\coqdocaxiom{int\_lt}} \coqdocvariable{n1} \coqdocvariable{n2})\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.bool eval le}{bool\_eval\_le}{\coqdocconstructor{bool\_eval\_le}}  : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}})(\coqdocvar{n1} \coqdocvar{n2}: \coqref{Lenguaje.ITs.Integer}{\coqdocaxiom{Integer}}),\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{e1} \coqdocvariable{n1} \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{e2} \coqdocvariable{n2} \ensuremath{\rightarrow} \coqref{Lenguaje.BoolEval}{\coqdocinductive{BoolEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.bool exp le}{\coqdocconstructor{bool\_exp\_le}} \coqdocvariable{e1} \coqdocvariable{e2}) (\coqref{Lenguaje.ITs.int le}{\coqdocaxiom{int\_le}} \coqdocvariable{n1} \coqdocvariable{n2})\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.bool eval gt}{bool\_eval\_gt}{\coqdocconstructor{bool\_eval\_gt}}  : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}})(\coqdocvar{n1} \coqdocvar{n2}: \coqref{Lenguaje.ITs.Integer}{\coqdocaxiom{Integer}}),\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{e1} \coqdocvariable{n1} \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{e2} \coqdocvariable{n2} \ensuremath{\rightarrow} \coqref{Lenguaje.BoolEval}{\coqdocinductive{BoolEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.bool exp gt}{\coqdocconstructor{bool\_exp\_gt}} \coqdocvariable{e1} \coqdocvariable{e2}) (\coqref{Lenguaje.ITs.int gt}{\coqdocaxiom{int\_gt}} \coqdocvariable{n1} \coqdocvariable{n2})\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{0.50em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.bool eval gtb}{bool\_eval\_gtb}{\coqdocconstructor{bool\_eval\_gtb}}  : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqref{Lenguaje.Lenguaje.ByteExp}{\coqdocinductive{ByteExp}})(\coqdocvar{n1} \coqdocvar{n2}: \coqref{Lenguaje.ITs.Byte}{\coqdocaxiom{Byte}}),\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.Lenguaje.ByteEval}{\coqdocinductive{ByteEval}} \coqdocvar{s} \coqdocvariable{e1} (\coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} \coqdocvariable{n1}) \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ByteEval}{\coqdocinductive{ByteEval}} \coqdocvar{s} \coqdocvariable{e2} (\coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} \coqdocvariable{n2}) \ensuremath{\rightarrow} \coqref{Lenguaje.BoolEval}{\coqdocinductive{BoolEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.bool exp gtb}{\coqdocconstructor{bool\_exp\_gtb}} \coqdocvariable{e1} \coqdocvariable{e2}) (\coqref{Lenguaje.ITs.byte gt}{\coqdocaxiom{byte\_gt}} \coqdocvariable{n1} \coqdocvariable{n2})\coqdoceol
\coqdocindent{0.50em}
\coqdoceol
\coqdocindent{0.50em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.bool eval eqb}{bool\_eval\_eqb}{\coqdocconstructor{bool\_eval\_eqb}}  : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqref{Lenguaje.Lenguaje.ByteExp}{\coqdocinductive{ByteExp}})(\coqdocvar{n1} \coqdocvar{n2}: \coqref{Lenguaje.ITs.Byte}{\coqdocaxiom{Byte}}),\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.Lenguaje.ByteEval}{\coqdocinductive{ByteEval}} \coqdocvar{s} \coqdocvariable{e1} (\coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} \coqdocvariable{n1}) \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ByteEval}{\coqdocinductive{ByteEval}} \coqdocvar{s} \coqdocvariable{e2} (\coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} \coqdocvariable{n2}) \ensuremath{\rightarrow} \coqref{Lenguaje.BoolEval}{\coqdocinductive{BoolEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.bool exp eqb}{\coqdocconstructor{bool\_exp\_eqb}} \coqdocvariable{e1} \coqdocvariable{e2}) (\coqref{Lenguaje.ITs.byte eq}{\coqdocaxiom{byte\_eq}} \coqdocvariable{n1} \coqdocvariable{n2})\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.bool eval ge}{bool\_eval\_ge}{\coqdocconstructor{bool\_eval\_ge}}  : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}})(\coqdocvar{n1} \coqdocvar{n2}: \coqref{Lenguaje.ITs.Integer}{\coqdocaxiom{Integer}}),\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{e1} \coqdocvariable{n1} \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{s} \coqdocvariable{e2} \coqdocvariable{n2} \ensuremath{\rightarrow} \coqref{Lenguaje.BoolEval}{\coqdocinductive{BoolEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.bool exp ge}{\coqdocconstructor{bool\_exp\_ge}} \coqdocvariable{e1} \coqdocvariable{e2}) (\coqref{Lenguaje.ITs.int ge}{\coqdocaxiom{int\_ge}} \coqdocvariable{n1} \coqdocvariable{n2})\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.bool eval not}{bool\_eval\_not}{\coqdocconstructor{bool\_eval\_not}} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1}: \coqref{Lenguaje.Lenguaje.BoolExp}{\coqdocinductive{BoolExp}})(\coqdocvar{b1}: \coqref{Lenguaje.ITs.Bool}{\coqdocaxiom{Bool}}),\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.BoolEval}{\coqdocinductive{BoolEval}} \coqdocvar{s} \coqdocvariable{e1} \coqdocvariable{b1} \ensuremath{\rightarrow} \coqref{Lenguaje.BoolEval}{\coqdocinductive{BoolEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.bool exp not}{\coqdocconstructor{bool\_exp\_not}} \coqdocvariable{e1}) (\coqref{Lenguaje.ITs.bool not}{\coqdocaxiom{bool\_not}} \coqdocvariable{b1})\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.bool eval and}{bool\_eval\_and}{\coqdocconstructor{bool\_eval\_and}} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqref{Lenguaje.Lenguaje.BoolExp}{\coqdocinductive{BoolExp}})(\coqdocvar{b1} \coqdocvar{b2}: \coqref{Lenguaje.ITs.Bool}{\coqdocaxiom{Bool}}),\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.BoolEval}{\coqdocinductive{BoolEval}} \coqdocvar{s} \coqdocvariable{e1} \coqdocvariable{b1} \ensuremath{\rightarrow} \coqref{Lenguaje.BoolEval}{\coqdocinductive{BoolEval}} \coqdocvar{s} \coqdocvariable{e2} \coqdocvariable{b2} \ensuremath{\rightarrow} \coqref{Lenguaje.BoolEval}{\coqdocinductive{BoolEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.bool exp and}{\coqdocconstructor{bool\_exp\_and}} \coqdocvariable{e1} \coqdocvariable{e2}) (\coqref{Lenguaje.ITs.bool and}{\coqdocaxiom{bool\_and}} \coqdocvariable{b1} \coqdocvariable{b2})\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.bool eval or}{bool\_eval\_or}{\coqdocconstructor{bool\_eval\_or}}  : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqref{Lenguaje.Lenguaje.BoolExp}{\coqdocinductive{BoolExp}})(\coqdocvar{b1} \coqdocvar{b2}: \coqref{Lenguaje.ITs.Bool}{\coqdocaxiom{Bool}}),\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.BoolEval}{\coqdocinductive{BoolEval}} \coqdocvar{s} \coqdocvariable{e1} \coqdocvariable{b1} \ensuremath{\rightarrow} \coqref{Lenguaje.BoolEval}{\coqdocinductive{BoolEval}} \coqdocvar{s} \coqdocvariable{e2} \coqdocvariable{b2} \ensuremath{\rightarrow} \coqref{Lenguaje.BoolEval}{\coqdocinductive{BoolEval}} \coqdocvar{s} (\coqref{Lenguaje.Lenguaje.bool exp or}{\coqdocconstructor{bool\_exp\_or}} \coqdocvariable{e1} \coqdocvariable{e2}) (\coqref{Lenguaje.ITs.bool or}{\coqdocaxiom{bool\_or}} \coqdocvariable{b1} \coqdocvariable{b2})\coqdoceol
\coqdocnoindent
.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Inductive} \coqdef{Lenguaje.Lenguaje.Instr}{Instr}{\coqdocinductive{Instr}} : \coqdockw{Type} :=\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.instr skip}{instr\_skip}{\coqdocconstructor{instr\_skip}}          : \coqref{Lenguaje.Instr}{\coqdocinductive{Instr}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.instr assign bool}{instr\_assign\_bool}{\coqdocconstructor{instr\_assign\_bool}}   : \coqref{Lenguaje.Lenguaje.Id}{\coqdocinductive{Id}}      \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.BoolExp}{\coqdocinductive{BoolExp}}   \ensuremath{\rightarrow} \coqref{Lenguaje.Instr}{\coqdocinductive{Instr}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.instr assign nat}{instr\_assign\_nat}{\coqdocconstructor{instr\_assign\_nat}}    : \coqref{Lenguaje.Lenguaje.Id}{\coqdocinductive{Id}}      \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}}  \ensuremath{\rightarrow} \coqref{Lenguaje.Instr}{\coqdocinductive{Instr}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.instr assign int}{instr\_assign\_int}{\coqdocconstructor{instr\_assign\_int}}    : \coqref{Lenguaje.Lenguaje.Id}{\coqdocinductive{Id}}      \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}}  \ensuremath{\rightarrow} \coqref{Lenguaje.Instr}{\coqdocinductive{Instr}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.instr assign byte}{instr\_assign\_byte}{\coqdocconstructor{instr\_assign\_byte}}   : \coqref{Lenguaje.Lenguaje.Id}{\coqdocinductive{Id}}      \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ByteExp}{\coqdocinductive{ByteExp}}   \ensuremath{\rightarrow} \coqref{Lenguaje.Instr}{\coqdocinductive{Instr}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.instr assign matrix}{instr\_assign\_matrix}{\coqdocconstructor{instr\_assign\_matrix}} : \coqref{Lenguaje.Lenguaje.Id}{\coqdocinductive{Id}}      \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.MatrixExp}{\coqdocinductive{MatrixExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.Instr}{\coqdocinductive{Instr}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.instr seq}{instr\_seq}{\coqdocconstructor{instr\_seq}}           : \coqref{Lenguaje.Instr}{\coqdocinductive{Instr}}   \ensuremath{\rightarrow} \coqref{Lenguaje.Instr}{\coqdocinductive{Instr}}     \ensuremath{\rightarrow} \coqref{Lenguaje.Instr}{\coqdocinductive{Instr}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.instr if}{instr\_if}{\coqdocconstructor{instr\_if}}            : \coqref{Lenguaje.Lenguaje.BoolExp}{\coqdocinductive{BoolExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.Instr}{\coqdocinductive{Instr}}     \ensuremath{\rightarrow} \coqref{Lenguaje.Instr}{\coqdocinductive{Instr}} \ensuremath{\rightarrow} \coqref{Lenguaje.Instr}{\coqdocinductive{Instr}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.instr while}{instr\_while}{\coqdocconstructor{instr\_while}}         : \coqref{Lenguaje.Lenguaje.BoolExp}{\coqdocinductive{BoolExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.Instr}{\coqdocinductive{Instr}}     \ensuremath{\rightarrow} \coqref{Lenguaje.Instr}{\coqdocinductive{Instr}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.instr for}{instr\_for}{\coqdocconstructor{instr\_for}}           : \coqref{Lenguaje.Lenguaje.Id}{\coqdocinductive{Id}}      \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}}  \ensuremath{\rightarrow} \coqref{Lenguaje.Instr}{\coqdocinductive{Instr}} \ensuremath{\rightarrow} \coqref{Lenguaje.Instr}{\coqdocinductive{Instr}}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.instr matrix set}{instr\_matrix\_set}{\coqdocconstructor{instr\_matrix\_set}}    : \coqref{Lenguaje.Lenguaje.Id}{\coqdocinductive{Id}}      \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}}  \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithExp}{\coqdocinductive{ArithExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ByteExp}{\coqdocinductive{ByteExp}} \ensuremath{\rightarrow} \coqref{Lenguaje.Instr}{\coqdocinductive{Instr}}\coqdoceol
\coqdocnoindent
.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Inductive} \coqdef{Lenguaje.Lenguaje.InstrEval}{InstrEval}{\coqdocinductive{InstrEval}} (\coqdocvar{st}: \coqref{Lenguaje.Lenguaje.State}{\coqdocdefinition{State}}) : \coqref{Lenguaje.Lenguaje.Instr}{\coqdocinductive{Instr}} \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.State}{\coqdocdefinition{State}} \ensuremath{\rightarrow} \coqdockw{Prop} :=\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.skip eval}{skip\_eval}{\coqdocconstructor{skip\_eval}} :\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.InstrEval}{\coqdocinductive{InstrEval}} \coqdocvar{st} \coqref{Lenguaje.Lenguaje.instr skip}{\coqdocconstructor{instr\_skip}} \coqdocvar{st}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.assign bool eval}{assign\_bool\_eval}{\coqdocconstructor{assign\_bool\_eval}} : \coqdockw{\ensuremath{\forall}} \coqdocvar{bid} \coqdocvar{bexp} \coqdocvar{b},\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.Lenguaje.BoolEval}{\coqdocinductive{BoolEval}} \coqdocvar{st} \coqdocvariable{bexp} \coqdocvariable{b} \ensuremath{\rightarrow} \coqref{Lenguaje.InstrEval}{\coqdocinductive{InstrEval}} \coqdocvar{st} (\coqref{Lenguaje.Lenguaje.instr assign bool}{\coqdocconstructor{instr\_assign\_bool}} \coqdocvariable{bid} \coqdocvariable{bexp}) (\coqref{Lenguaje.Lenguaje.Update}{\coqdocdefinition{Update}} \coqdocvar{st} \coqdocvariable{bid} (\coqref{Lenguaje.Lenguaje.bool val}{\coqdocconstructor{bool\_val}} \coqdocvariable{b}))\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.assign int eval}{assign\_int\_eval}{\coqdocconstructor{assign\_int\_eval}} : \coqdockw{\ensuremath{\forall}} \coqdocvar{zid} \coqdocvar{zexp} \coqdocvar{z},\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{st} \coqdocvariable{zexp} \coqdocvariable{z} \ensuremath{\rightarrow} \coqref{Lenguaje.InstrEval}{\coqdocinductive{InstrEval}} \coqdocvar{st} (\coqref{Lenguaje.Lenguaje.instr assign int}{\coqdocconstructor{instr\_assign\_int}} \coqdocvariable{zid} \coqdocvariable{zexp}) (\coqref{Lenguaje.Lenguaje.Update}{\coqdocdefinition{Update}} \coqdocvar{st} \coqdocvariable{zid} (\coqref{Lenguaje.Lenguaje.int val}{\coqdocconstructor{int\_val}} \coqdocvariable{z}))\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.assign byte eval}{assign\_byte\_eval}{\coqdocconstructor{assign\_byte\_eval}} : \coqdockw{\ensuremath{\forall}} \coqdocvar{bid} \coqdocvar{bexp} \coqdocvar{b},\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.Lenguaje.ByteEval}{\coqdocinductive{ByteEval}} \coqdocvar{st} \coqdocvariable{bexp} (\coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} \coqdocvariable{b}) \ensuremath{\rightarrow} \coqref{Lenguaje.InstrEval}{\coqdocinductive{InstrEval}} \coqdocvar{st} (\coqref{Lenguaje.Lenguaje.instr assign byte}{\coqdocconstructor{instr\_assign\_byte}} \coqdocvariable{bid} \coqdocvariable{bexp}) (\coqref{Lenguaje.Lenguaje.Update}{\coqdocdefinition{Update}} \coqdocvar{st} \coqdocvariable{bid} (\coqref{Lenguaje.Lenguaje.byte val}{\coqdocconstructor{byte\_val}} \coqdocvariable{b}))\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.assign matrix eval}{assign\_matrix\_eval}{\coqdocconstructor{assign\_matrix\_eval}} : \coqdockw{\ensuremath{\forall}} \coqdocvar{mid} (\coqdocvar{m} \coqdocvar{n}: \coqref{Lenguaje.ITs.Integer}{\coqdocaxiom{Integer}}) (\coqdocvar{matr}: \coqref{Lenguaje.ITs.Matrix}{\coqdocaxiom{Matrix}} \coqref{Lenguaje.ITs.Byte}{\coqdocaxiom{Byte}} \coqdocvariable{m} \coqdocvariable{n}) (\coqdocvar{mexp} : \coqref{Lenguaje.Lenguaje.MatrixExp}{\coqdocinductive{MatrixExp}}),\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.Lenguaje.MatrixEval}{\coqdocinductive{MatrixEval}} \coqdocvar{st} \coqdocvariable{mexp} \coqdocvariable{matr} \ensuremath{\rightarrow} \coqref{Lenguaje.InstrEval}{\coqdocinductive{InstrEval}} \coqdocvar{st} (\coqref{Lenguaje.Lenguaje.instr assign matrix}{\coqdocconstructor{instr\_assign\_matrix}} \coqdocvariable{mid} \coqdocvariable{mexp}) (\coqref{Lenguaje.Lenguaje.Update}{\coqdocdefinition{Update}} \coqdocvar{st} \coqdocvariable{mid} (\coqref{Lenguaje.Lenguaje.byte matrix val}{\coqdocconstructor{byte\_matrix\_val}} \coqdocvariable{matr}))\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.seq eval}{seq\_eval}{\coqdocconstructor{seq\_eval}} : \coqdockw{\ensuremath{\forall}} \coqdocvar{i1} \coqdocvar{i2} \coqdocvar{st'} \coqdocvar{st'{}'},\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.InstrEval}{\coqdocinductive{InstrEval}} \coqdocvar{st} \coqdocvariable{i1} \coqdocvariable{st'} \ensuremath{\rightarrow} \coqref{Lenguaje.InstrEval}{\coqdocinductive{InstrEval}} \coqdocvariable{st'} \coqdocvariable{i2} \coqdocvariable{st'{}'} \ensuremath{\rightarrow} \coqref{Lenguaje.InstrEval}{\coqdocinductive{InstrEval}} \coqdocvar{st} (\coqref{Lenguaje.Lenguaje.instr seq}{\coqdocconstructor{instr\_seq}} \coqdocvariable{i1} \coqdocvariable{i2}) \coqdocvariable{st'{}'}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.if eval true}{if\_eval\_true}{\coqdocconstructor{if\_eval\_true}} : \coqdockw{\ensuremath{\forall}} \coqdocvar{bexp} \coqdocvar{i1} \coqdocvar{i2} \coqdocvar{st'},\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.Lenguaje.BoolEval}{\coqdocinductive{BoolEval}} \coqdocvar{st} \coqdocvariable{bexp} \coqref{Lenguaje.ITs.TRUE}{\coqdocaxiom{TRUE}} \ensuremath{\rightarrow} \coqref{Lenguaje.InstrEval}{\coqdocinductive{InstrEval}} \coqdocvar{st} \coqdocvariable{i1} \coqdocvariable{st'} \ensuremath{\rightarrow} \coqref{Lenguaje.InstrEval}{\coqdocinductive{InstrEval}} \coqdocvar{st} (\coqref{Lenguaje.Lenguaje.instr if}{\coqdocconstructor{instr\_if}} \coqdocvariable{bexp} \coqdocvariable{i1} \coqdocvariable{i2}) \coqdocvariable{st'}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.if eval false}{if\_eval\_false}{\coqdocconstructor{if\_eval\_false}} : \coqdockw{\ensuremath{\forall}} \coqdocvar{bexp} \coqdocvar{i1} \coqdocvar{i2} \coqdocvar{st'},\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.Lenguaje.BoolEval}{\coqdocinductive{BoolEval}} \coqdocvar{st} \coqdocvariable{bexp} \coqref{Lenguaje.ITs.FALSE}{\coqdocaxiom{FALSE}} \ensuremath{\rightarrow} \coqref{Lenguaje.InstrEval}{\coqdocinductive{InstrEval}} \coqdocvar{st} \coqdocvariable{i2} \coqdocvariable{st'} \ensuremath{\rightarrow} \coqref{Lenguaje.InstrEval}{\coqdocinductive{InstrEval}} \coqdocvar{st} (\coqref{Lenguaje.Lenguaje.instr if}{\coqdocconstructor{instr\_if}} \coqdocvariable{bexp} \coqdocvariable{i1} \coqdocvariable{i2}) \coqdocvariable{st'}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.while eval true}{while\_eval\_true}{\coqdocconstructor{while\_eval\_true}} : \coqdockw{\ensuremath{\forall}} \coqdocvar{bexp} \coqdocvar{i} \coqdocvar{st'} \coqdocvar{st'{}'},\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.Lenguaje.BoolEval}{\coqdocinductive{BoolEval}} \coqdocvar{st} \coqdocvariable{bexp} \coqref{Lenguaje.ITs.TRUE}{\coqdocaxiom{TRUE}} \ensuremath{\rightarrow} \coqref{Lenguaje.InstrEval}{\coqdocinductive{InstrEval}} \coqdocvar{st} \coqdocvariable{i} \coqdocvariable{st'} \ensuremath{\rightarrow} \coqref{Lenguaje.InstrEval}{\coqdocinductive{InstrEval}} \coqdocvariable{st'} (\coqref{Lenguaje.Lenguaje.instr while}{\coqdocconstructor{instr\_while}} \coqdocvariable{bexp} \coqdocvariable{i}) \coqdocvariable{st'{}'} \ensuremath{\rightarrow} \coqref{Lenguaje.InstrEval}{\coqdocinductive{InstrEval}} \coqdocvar{st} (\coqref{Lenguaje.Lenguaje.instr while}{\coqdocconstructor{instr\_while}} \coqdocvariable{bexp} \coqdocvariable{i}) \coqdocvariable{st'{}'}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.while eval false}{while\_eval\_false}{\coqdocconstructor{while\_eval\_false}} : \coqdockw{\ensuremath{\forall}} \coqdocvar{bexp} \coqdocvar{i},\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.Lenguaje.BoolEval}{\coqdocinductive{BoolEval}} \coqdocvar{st} \coqdocvariable{bexp} \coqref{Lenguaje.ITs.FALSE}{\coqdocaxiom{FALSE}} \ensuremath{\rightarrow} \coqref{Lenguaje.InstrEval}{\coqdocinductive{InstrEval}} \coqdocvar{st} (\coqref{Lenguaje.Lenguaje.instr while}{\coqdocconstructor{instr\_while}} \coqdocvariable{bexp} \coqdocvariable{i}) \coqdocvar{st}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.for eval end}{for\_eval\_end}{\coqdocconstructor{for\_eval\_end}} : \coqdockw{\ensuremath{\forall}} \coqdocvar{i} \coqdocvar{n} \coqdocvar{instr},\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.Lenguaje.BoolEval}{\coqdocinductive{BoolEval}} \coqdocvar{st} (\coqref{Lenguaje.Lenguaje.bool exp ge}{\coqdocconstructor{bool\_exp\_ge}} (\coqref{Lenguaje.Lenguaje.arith exp id}{\coqdocconstructor{arith\_exp\_id}} \coqdocvariable{i}) \coqdocvariable{n}) \coqref{Lenguaje.ITs.TRUE}{\coqdocaxiom{TRUE}} \ensuremath{\rightarrow} \coqref{Lenguaje.InstrEval}{\coqdocinductive{InstrEval}} \coqdocvar{st} (\coqref{Lenguaje.Lenguaje.instr for}{\coqdocconstructor{instr\_for}} \coqdocvariable{i} \coqdocvariable{n} \coqdocvariable{instr}) \coqdocvar{st}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.for eval step}{for\_eval\_step}{\coqdocconstructor{for\_eval\_step}} : \coqdockw{\ensuremath{\forall}} \coqdocvar{i} \coqdocvar{x} \coqdocvar{n} \coqdocvar{instr} \coqdocvar{st'} \coqdocvar{st'{}'},\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.Lenguaje.BoolEval}{\coqdocinductive{BoolEval}} \coqdocvar{st} (\coqref{Lenguaje.Lenguaje.bool exp lt}{\coqdocconstructor{bool\_exp\_lt}} (\coqref{Lenguaje.Lenguaje.arith exp id}{\coqdocconstructor{arith\_exp\_id}} \coqdocvariable{i}) \coqdocvariable{n}) \coqref{Lenguaje.ITs.TRUE}{\coqdocaxiom{TRUE}} \ensuremath{\rightarrow} \coqref{Lenguaje.InstrEval}{\coqdocinductive{InstrEval}} \coqdocvar{st} \coqdocvariable{instr} \coqdocvariable{st'} \ensuremath{\rightarrow} \coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.InstrEval}{\coqdocinductive{InstrEval}} \coqdocvariable{st'} (\coqref{Lenguaje.Lenguaje.instr for}{\coqdocconstructor{instr\_for}} \coqdocvariable{i} \coqdocvariable{n} \coqdocvariable{instr}) \coqdocvariable{st'{}'} \ensuremath{\rightarrow} \coqdocvariable{st'} \coqdocvariable{i} \coqexternalref{:type scope:x '=' x}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Logic}{\coqdocnotation{=}} \coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} (\coqref{Lenguaje.Lenguaje.int val}{\coqdocconstructor{int\_val}} \coqdocvariable{x}) \ensuremath{\rightarrow} \coqdocvariable{st'{}'} \coqdocvariable{i} \coqexternalref{:type scope:x '=' x}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Logic}{\coqdocnotation{=}} \coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} (\coqref{Lenguaje.Lenguaje.int val}{\coqdocconstructor{int\_val}} (\coqref{Lenguaje.ITs.int plus}{\coqdocaxiom{int\_plus}} \coqdocvariable{x} \coqref{Lenguaje.ITs.ONE}{\coqdocaxiom{ONE}})) \ensuremath{\rightarrow}\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.InstrEval}{\coqdocinductive{InstrEval}} \coqdocvar{st} (\coqref{Lenguaje.Lenguaje.instr for}{\coqdocconstructor{instr\_for}} \coqdocvariable{i} \coqdocvariable{n} \coqdocvariable{instr}) \coqdocvariable{st'{}'}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdef{Lenguaje.Lenguaje.matrix set eval}{matrix\_set\_eval}{\coqdocconstructor{matrix\_set\_eval}} : \coqdockw{\ensuremath{\forall}} \coqdocvar{m} \coqdocvar{n} \coqdocvar{i} \coqdocvar{j} \coqdocvar{e1} \coqdocvar{e2} \coqdocvar{e} \coqdocvar{mid} (\coqdocvar{matr} \coqdocvar{matr'}: \coqref{Lenguaje.ITs.Matrix}{\coqdocaxiom{Matrix}} \coqref{Lenguaje.ITs.Byte}{\coqdocaxiom{Byte}} \coqdocvariable{m} \coqdocvariable{n}) \coqdocvar{b},\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.Lenguaje.MatrixEval}{\coqdocinductive{MatrixEval}} \coqdocvar{st} (\coqref{Lenguaje.Lenguaje.matrix exp id}{\coqdocconstructor{matrix\_exp\_id}} \coqdocvariable{mid}) \coqdocvariable{matr} \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{st} \coqdocvariable{e1} \coqdocvariable{i} \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ArithEval}{\coqdocinductive{ArithEval}} \coqdocvar{st} \coqdocvariable{e2} \coqdocvariable{j} \ensuremath{\rightarrow} \coqref{Lenguaje.Lenguaje.ByteEval}{\coqdocinductive{ByteEval}} \coqdocvar{st} \coqdocvariable{e} (\coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} \coqdocvariable{b}) \ensuremath{\rightarrow} \coqref{Lenguaje.ITs.matrix set}{\coqdocaxiom{matrix\_set}} \coqdocvariable{matr} \coqdocvariable{i} \coqdocvariable{j} \coqdocvariable{b} \coqexternalref{:type scope:x '=' x}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Logic}{\coqdocnotation{=}} \coqexternalref{Some}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} \coqdocvariable{matr'} \ensuremath{\rightarrow}\coqdoceol
\coqdocindent{3.00em}
\coqref{Lenguaje.InstrEval}{\coqdocinductive{InstrEval}} \coqdocvar{st} (\coqref{Lenguaje.Lenguaje.instr matrix set}{\coqdocconstructor{instr\_matrix\_set}} \coqdocvariable{mid} \coqdocvariable{e1} \coqdocvariable{e2} \coqdocvariable{e}) (\coqref{Lenguaje.Lenguaje.Update}{\coqdocdefinition{Update}} \coqdocvar{st} \coqdocvariable{mid} (\coqref{Lenguaje.Lenguaje.byte matrix val}{\coqdocconstructor{byte\_matrix\_val}} \coqdocvariable{matr'}))\coqdoceol
\coqdocnoindent
.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Notation} \coqdef{Lenguaje.Lenguaje.::x '/' x '||' x}{"}{"}c1 / st || st'" := (\coqref{Lenguaje.Lenguaje.InstrEval}{\coqdocinductive{InstrEval}} \coqdocvar{st} \coqdocvar{c1} \coqdocvar{st'}) (\coqdoctac{at} \coqdockw{level} 40, \coqdocvar{st} \coqdoctac{at} \coqdockw{level} 39).\coqdoceol
\coqdocnoindent
\coqdockw{Notation} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:'SKIP'}{"}{"}'SKIP'" := \coqref{Lenguaje.Lenguaje.instr skip}{\coqdocconstructor{instr\_skip}} : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocnoindent
\coqdockw{Notation} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:'bool' x '::=' x}{"}{"}'bool' X ::= a" :=\coqdoceol
\coqdocindent{1.00em}
(\coqref{Lenguaje.Lenguaje.instr assign bool}{\coqdocconstructor{instr\_assign\_bool}} \coqdocvar{X} \coqdocvar{a}) (\coqdoctac{at} \coqdockw{level} 80, \coqdoctac{left} \coqdockw{associativity}) : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocnoindent
\coqdockw{Notation} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:'int' x '::=' x}{"}{"}'int' X ::= a" :=\coqdoceol
\coqdocindent{1.00em}
(\coqref{Lenguaje.Lenguaje.instr assign int}{\coqdocconstructor{instr\_assign\_int}} \coqdocvar{X} \coqdocvar{a}) (\coqdoctac{at} \coqdockw{level} 80, \coqdoctac{left} \coqdockw{associativity}) : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocnoindent
\coqdockw{Notation} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:'byte' x '::=' x}{"}{"}'byte' X ::= a" :=\coqdoceol
\coqdocindent{1.00em}
(\coqref{Lenguaje.Lenguaje.instr assign byte}{\coqdocconstructor{instr\_assign\_byte}} \coqdocvar{X} \coqdocvar{a}) (\coqdoctac{at} \coqdockw{level} 80, \coqdoctac{left} \coqdockw{associativity}) : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocnoindent
\coqdockw{Notation} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:'matrix' x '::=' x}{"}{"}'matrix' X ::= a" :=\coqdoceol
\coqdocindent{1.00em}
(\coqref{Lenguaje.Lenguaje.instr assign matrix}{\coqdocconstructor{instr\_assign\_matrix}} \coqdocvar{X} \coqdocvar{a}) (\coqdoctac{at} \coqdockw{level} 80, \coqdoctac{left} \coqdockw{associativity}) : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocnoindent
\coqdockw{Notation} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:x '[' x '][' x ']' '::=' x}{"}{"}m [ i ][ j ] ::= x" :=\coqdoceol
\coqdocindent{1.00em}
(\coqref{Lenguaje.Lenguaje.instr matrix set}{\coqdocconstructor{instr\_matrix\_set}} \coqdocvar{m} \coqdocvar{i} \coqdocvar{j} \coqdocvar{x}) (\coqdoctac{at} \coqdockw{level} 70, \coqdocvar{x} \coqdoctac{at} \coqdocvar{next} \coqdockw{level}, \coqdoctac{right} \coqdockw{associativity}) : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocnoindent
\coqdockw{Notation} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:x ';' x}{"}{"}c1 ; c2" :=\coqdoceol
\coqdocindent{1.00em}
(\coqref{Lenguaje.Lenguaje.instr seq}{\coqdocconstructor{instr\_seq}} \coqdocvar{c1} \coqdocvar{c2}) (\coqdoctac{at} \coqdockw{level} 80, \coqdoctac{right} \coqdockw{associativity}) : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocnoindent
\coqdockw{Notation} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:x ';'}{"}{"}c1 ;" :=\coqdoceol
\coqdocindent{1.00em}
(\coqdocvar{c1}) (\coqdoctac{at} \coqdockw{level} 80, \coqdoctac{right} \coqdockw{associativity}) : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocnoindent
\coqdockw{Notation} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:'WHILE' x 'DO' x 'END'}{"}{"}'WHILE' b 'DO' c 'END'" :=\coqdoceol
\coqdocindent{1.00em}
(\coqref{Lenguaje.Lenguaje.instr while}{\coqdocconstructor{instr\_while}} \coqdocvar{b} \coqdocvar{c}) (\coqdoctac{at} \coqdockw{level} 80, \coqdoctac{right} \coqdockw{associativity}) : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocnoindent
\coqdockw{Notation} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:'FOR' x 'TO' x 'DO' x 'END'}{"}{"}'FOR' b 'TO' c 'DO' d 'END'" :=\coqdoceol
\coqdocindent{1.00em}
(\coqref{Lenguaje.Lenguaje.instr for}{\coqdocconstructor{instr\_for}} \coqdocvar{b} \coqdocvar{c} \coqdocvar{d}) (\coqdoctac{at} \coqdockw{level} 80, \coqdoctac{right} \coqdockw{associativity}) : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocnoindent
\coqdockw{Notation} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:'IFB' x 'THEN' x 'ELSE' x 'END'}{"}{"}'IFB' c1 'THEN' c2 'ELSE' c3 'END'" := (\coqref{Lenguaje.Lenguaje.instr if}{\coqdocconstructor{instr\_if}} \coqdocvar{c1} \coqdocvar{c2} \coqdocvar{c3})(\coqdoctac{at} \coqdockw{level} 80, \coqdoctac{right} \coqdockw{associativity}) : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocnoindent
\coqdockw{Notation} \coqdef{Lenguaje.Lenguaje.:lenguaje scope:'IFB' x 'THEN' x 'END'}{"}{"}'IFB' e1 'THEN' e2 'END'" :=\coqdoceol
\coqdocindent{1.00em}
(\coqref{Lenguaje.Lenguaje.instr if}{\coqdocconstructor{instr\_if}} \coqdocvar{e1} \coqdocvar{e2} \coqref{Lenguaje.Lenguaje.instr skip}{\coqdocconstructor{instr\_skip}}) (\coqdoctac{at} \coqdockw{level} 80, \coqdoctac{right} \coqdockw{associativity}) : \coqdocvar{lenguaje\_scope}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{End} \coqref{Lenguaje}{\coqdocmodule{Lenguaje}}.\coqdoceol
\end{coqdoccode}
\end{document}
